minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
↳ QTRS
↳ DependencyPairsProof
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
DIV_ACTIVE2(s1(x), s1(y)) -> GE_ACTIVE2(x, y)
IF_ACTIVE3(true, x, y) -> MARK1(x)
GE_ACTIVE2(s1(x), s1(y)) -> GE_ACTIVE2(x, y)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
MARK1(if3(x, y, z)) -> MARK1(x)
MARK1(s1(x)) -> MARK1(x)
MARK1(ge2(x, y)) -> GE_ACTIVE2(x, y)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
MARK1(div2(x, y)) -> MARK1(x)
MARK1(minus2(x, y)) -> MINUS_ACTIVE2(x, y)
MINUS_ACTIVE2(s1(x), s1(y)) -> MINUS_ACTIVE2(x, y)
IF_ACTIVE3(false, x, y) -> MARK1(y)
MARK1(if3(x, y, z)) -> IF_ACTIVE3(mark1(x), y, z)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
DIV_ACTIVE2(s1(x), s1(y)) -> GE_ACTIVE2(x, y)
IF_ACTIVE3(true, x, y) -> MARK1(x)
GE_ACTIVE2(s1(x), s1(y)) -> GE_ACTIVE2(x, y)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
MARK1(if3(x, y, z)) -> MARK1(x)
MARK1(s1(x)) -> MARK1(x)
MARK1(ge2(x, y)) -> GE_ACTIVE2(x, y)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
MARK1(div2(x, y)) -> MARK1(x)
MARK1(minus2(x, y)) -> MINUS_ACTIVE2(x, y)
MINUS_ACTIVE2(s1(x), s1(y)) -> MINUS_ACTIVE2(x, y)
IF_ACTIVE3(false, x, y) -> MARK1(y)
MARK1(if3(x, y, z)) -> IF_ACTIVE3(mark1(x), y, z)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
GE_ACTIVE2(s1(x), s1(y)) -> GE_ACTIVE2(x, y)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GE_ACTIVE2(s1(x), s1(y)) -> GE_ACTIVE2(x, y)
POL(GE_ACTIVE2(x1, x2)) = x2
POL(s1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
MINUS_ACTIVE2(s1(x), s1(y)) -> MINUS_ACTIVE2(x, y)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS_ACTIVE2(s1(x), s1(y)) -> MINUS_ACTIVE2(x, y)
POL(MINUS_ACTIVE2(x1, x2)) = x2
POL(s1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
MARK1(if3(x, y, z)) -> MARK1(x)
MARK1(s1(x)) -> MARK1(x)
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
MARK1(div2(x, y)) -> MARK1(x)
IF_ACTIVE3(false, x, y) -> MARK1(y)
MARK1(if3(x, y, z)) -> IF_ACTIVE3(mark1(x), y, z)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK1(if3(x, y, z)) -> MARK1(x)
MARK1(if3(x, y, z)) -> IF_ACTIVE3(mark1(x), y, z)
Used ordering: Polynomial interpretation [21]:
MARK1(s1(x)) -> MARK1(x)
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
MARK1(div2(x, y)) -> MARK1(x)
IF_ACTIVE3(false, x, y) -> MARK1(y)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
POL(0) = 0
POL(DIV_ACTIVE2(x1, x2)) = 0
POL(IF_ACTIVE3(x1, x2, x3)) = x2 + x3
POL(MARK1(x1)) = x1
POL(div2(x1, x2)) = x1
POL(div_active2(x1, x2)) = 0
POL(false) = 0
POL(ge2(x1, x2)) = 0
POL(ge_active2(x1, x2)) = 0
POL(if3(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(if_active3(x1, x2, x3)) = 0
POL(mark1(x1)) = 0
POL(minus2(x1, x2)) = 0
POL(minus_active2(x1, x2)) = 0
POL(s1(x1)) = x1
POL(true) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
MARK1(s1(x)) -> MARK1(x)
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
MARK1(div2(x, y)) -> MARK1(x)
IF_ACTIVE3(false, x, y) -> MARK1(y)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK1(div2(x, y)) -> MARK1(x)
Used ordering: Polynomial interpretation [21]:
MARK1(s1(x)) -> MARK1(x)
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
IF_ACTIVE3(false, x, y) -> MARK1(y)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
POL(0) = 0
POL(DIV_ACTIVE2(x1, x2)) = 1
POL(IF_ACTIVE3(x1, x2, x3)) = x2 + x3
POL(MARK1(x1)) = x1
POL(div2(x1, x2)) = 1 + x1
POL(div_active2(x1, x2)) = 0
POL(false) = 0
POL(ge2(x1, x2)) = 0
POL(ge_active2(x1, x2)) = x1 + x2
POL(if3(x1, x2, x3)) = 0
POL(if_active3(x1, x2, x3)) = 0
POL(mark1(x1)) = 0
POL(minus2(x1, x2)) = 0
POL(minus_active2(x1, x2)) = 0
POL(s1(x1)) = x1
POL(true) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
MARK1(s1(x)) -> MARK1(x)
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
IF_ACTIVE3(false, x, y) -> MARK1(y)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK1(s1(x)) -> MARK1(x)
Used ordering: Polynomial interpretation [21]:
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
IF_ACTIVE3(false, x, y) -> MARK1(y)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
POL(0) = 0
POL(DIV_ACTIVE2(x1, x2)) = 1 + x1
POL(IF_ACTIVE3(x1, x2, x3)) = x1 + x2 + x3
POL(MARK1(x1)) = 1 + x1
POL(div2(x1, x2)) = x1
POL(div_active2(x1, x2)) = x1
POL(false) = 1
POL(ge2(x1, x2)) = 1
POL(ge_active2(x1, x2)) = 1
POL(if3(x1, x2, x3)) = x2 + x3
POL(if_active3(x1, x2, x3)) = x2 + x3
POL(mark1(x1)) = x1
POL(minus2(x1, x2)) = 0
POL(minus_active2(x1, x2)) = 0
POL(s1(x1)) = 1 + x1
POL(true) = 1
minus_active2(0, y) -> 0
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(x, 0) -> true
mark1(0) -> 0
ge_active2(0, s1(y)) -> false
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(x, y) -> ge2(x, y)
minus_active2(x, y) -> minus2(x, y)
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(0, s1(y)) -> 0
div_active2(x, y) -> div2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
if_active3(true, x, y) -> mark1(x)
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
if_active3(false, x, y) -> mark1(y)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
IF_ACTIVE3(false, x, y) -> MARK1(y)
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV_ACTIVE2(s1(x), s1(y)) -> IF_ACTIVE3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
Used ordering: Polynomial interpretation [21]:
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
IF_ACTIVE3(false, x, y) -> MARK1(y)
POL(0) = 0
POL(DIV_ACTIVE2(x1, x2)) = 1 + x2
POL(IF_ACTIVE3(x1, x2, x3)) = x1 + x2 + x3
POL(MARK1(x1)) = x1
POL(div2(x1, x2)) = 1 + x1 + x2
POL(div_active2(x1, x2)) = 0
POL(false) = 0
POL(ge2(x1, x2)) = 0
POL(ge_active2(x1, x2)) = 0
POL(if3(x1, x2, x3)) = 0
POL(if_active3(x1, x2, x3)) = 0
POL(mark1(x1)) = 0
POL(minus2(x1, x2)) = 0
POL(minus_active2(x1, x2)) = 0
POL(s1(x1)) = 1
POL(true) = 0
ge_active2(x, 0) -> true
ge_active2(0, s1(y)) -> false
ge_active2(x, y) -> ge2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
IF_ACTIVE3(true, x, y) -> MARK1(x)
MARK1(div2(x, y)) -> DIV_ACTIVE2(mark1(x), y)
IF_ACTIVE3(false, x, y) -> MARK1(y)
minus_active2(0, y) -> 0
mark1(0) -> 0
minus_active2(s1(x), s1(y)) -> minus_active2(x, y)
mark1(s1(x)) -> s1(mark1(x))
ge_active2(x, 0) -> true
mark1(minus2(x, y)) -> minus_active2(x, y)
ge_active2(0, s1(y)) -> false
mark1(ge2(x, y)) -> ge_active2(x, y)
ge_active2(s1(x), s1(y)) -> ge_active2(x, y)
mark1(div2(x, y)) -> div_active2(mark1(x), y)
div_active2(0, s1(y)) -> 0
mark1(if3(x, y, z)) -> if_active3(mark1(x), y, z)
div_active2(s1(x), s1(y)) -> if_active3(ge_active2(x, y), s1(div2(minus2(x, y), s1(y))), 0)
if_active3(true, x, y) -> mark1(x)
minus_active2(x, y) -> minus2(x, y)
if_active3(false, x, y) -> mark1(y)
ge_active2(x, y) -> ge2(x, y)
if_active3(x, y, z) -> if3(x, y, z)
div_active2(x, y) -> div2(x, y)